|
|
Invarianty jetových grup a aplikace v mechanice kontinua
Buriánek, Martin ; Doupovec, Miroslav (oponent) ; Kureš, Miroslav (vedoucí práce)
Tato práce se zabývá jetovými grupami a jejich maticovými reprezentacemi. V úvodní části práce se věnujeme reprezentacím grup, akcím grup na množinách a invariantům akcí. V další části jsou objasněny pojmy hladká varieta, Lieova grupa a Lieova algebra. Následuje vysvětlení pojmu jet a zavedení jetové grupy jako speciálního případu Lieovy grupy. Nejprve jsou popsány grupy $G_1^r$ a $G_n^1$, poté grupa $G_n^2$ a její podgrupy. U popsaných jetových grup jsou navrženy jejich reprezentace. V závěru práce je nástíněna možnost aplikací jetových grup v mechanice kontinua. Práce je doplněna algoritmizací vybraných problému v softwaru Wolfram Mathematica.
|
|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose a way to improve precision of program analysis in the 2LS framework, based on its existing concepts, mainly template-based synthesis of invariants. 2LS is a static analysis framework for analysing C programs which relies on the use of an SMT solver and of abstract interpretation for automatic invariant inference. In a case when 2LS can not decide whether a program is correct, the proposed solution analyses the invariants computed in various abstract domains and identifies parts of the invariants that potentially cause undecidability of the verification. Using the obtained information, the designed method is able to identify variables of the original program that possibly determine whether the verification is successful. The output of our solution can be used as a feedback to indicate variables with problematic values that should be constrained. Also, it can be utilized by the 2LS developers for debugging purposes during development of new analyses. The solution has been implemented in the 2LS framework. Testing our solution on various benchmarks from the International Competition on Software Verification (SV-COMP) shows that it can identify variables that cause undecidability of the verification in more than half of the programs where the verification currently fails.
|
|
|
Využití invariantů geometrických transformací k řešení úloh
Doubrava, Jiří ; Zamboj, Michal (vedoucí práce) ; Beran, Filip (oponent)
Práce se zabývá rozdělením vzájemně jednoznačných kolineárních geometrických zob- razení. Zabývá se tomuto rozdělení odpovídajícím pohledem na zadání i řešení úloh. Hlavní částí práce je sbírka řešených úloh z oblasti rovinné geometrie, které jsou rozdě- leny do několika skupin. Práce může být použita jak učiteli matematiky na středních ško- lách, tak samotnými středoškoláky. Práce je rozdělena do dvou částí; první část je teore- tická a obsahuje stručné seznámení se základními pojmy týkajícími se invariantů geome- trických transformací a popis struktury geometrie podle Felixe Kleina včetně jeho Erlan- genského programu; druhá část obsahuje samotná zadání a řešení úloh. Řešení některých uvedených úloh jsou pro lepší názornost doplněna obrázky vytvořenými v programu Ge- oGebra. Obrázky hrají svou roli i v teoretické části, kde mohou napomoci k lepšímu po- chopení některých složitějších pojmů. Některé z použitých úloh jsou autorské, jiné jsou převzaté z různých pramenů uvedených v seznamu použitých zdrojů. KLÍČOVÁ SLOVA geometrické transformace, grupy, Erlangenský program, invariant, řešené úlohy
|
|
|
Invarianty jetových grup a aplikace v mechanice kontinua
Buriánek, Martin ; Doupovec, Miroslav (oponent) ; Kureš, Miroslav (vedoucí práce)
Tato práce se zabývá jetovými grupami a jejich maticovými reprezentacemi. V úvodní části práce se věnujeme reprezentacím grup, akcím grup na množinách a invariantům akcí. V další části jsou objasněny pojmy hladká varieta, Lieova grupa a Lieova algebra. Následuje vysvětlení pojmu jet a zavedení jetové grupy jako speciálního případu Lieovy grupy. Nejprve jsou popsány grupy $G_1^r$ a $G_n^1$, poté grupa $G_n^2$ a její podgrupy. U popsaných jetových grup jsou navrženy jejich reprezentace. V závěru práce je nástíněna možnost aplikací jetových grup v mechanice kontinua. Práce je doplněna algoritmizací vybraných problému v softwaru Wolfram Mathematica.
|
|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose a way to improve precision of program analysis in the 2LS framework, based on its existing concepts, mainly template-based synthesis of invariants. 2LS is a static analysis framework for analysing C programs which relies on the use of an SMT solver and of abstract interpretation for automatic invariant inference. In a case when 2LS can not decide whether a program is correct, the proposed solution analyses the invariants computed in various abstract domains and identifies parts of the invariants that potentially cause undecidability of the verification. Using the obtained information, the designed method is able to identify variables of the original program that possibly determine whether the verification is successful. The output of our solution can be used as a feedback to indicate variables with problematic values that should be constrained. Also, it can be utilized by the 2LS developers for debugging purposes during development of new analyses. The solution has been implemented in the 2LS framework. Testing our solution on various benchmarks from the International Competition on Software Verification (SV-COMP) shows that it can identify variables that cause undecidability of the verification in more than half of the programs where the verification currently fails.
|
|
|
Platónova vize ideálního státu v pozadí negativních utopií ve 20. století
LACUŠKOVÁ, Petra
V této diplomové práci se budu zabývat komparací Platónovy vize ideálního státu nastíněné v jeho díle Ústava s negativními utopiemi vzniklými ve 20. století. Za pomocí strukturální analýzy, kterou navrhl Claude Lévi-Strauss, budu hledat společné invarianty vyskytující se ve všech předložených dílech. Předmětem mého zkoumání budou knihy Ústava, My, Konec civilizace, 1984 a filmy Metropolis, Matrix a Equilibrium. Na závěr práce předložím svou hypotézu, podle které je dalším invariantem fakt, že všechny fikční světy mnou zkoumaných děl jsou založeny na posilování ekonomického charakteru člověka kvůli snaze maximalizovat jeho efektivitu coby pouhé výrobní jednotky. Což se děje pomocí umělého potlačování a ničení přirozené Zkušenosti, o které mluví John Dewey.
|
host ::
RSS.